$\forall$${\it es}$:ES, $A$:Type, $I$:AbsInterface($A$).
\\[0ex]$I$ is local
\\[0ex]$\Rightarrow$ $I$ is finite
\\[0ex]$\Rightarrow$ ($\exists$$X$:MaInterface($A$). (ma{-}interface{-}consistent(${\it es}$;$X$) \& [[$X$]] = $I$))